\begin{tabbing}
fun{-}path($T$;$f$;$L$;$y$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(0 $<$ $\parallel$$L$$\parallel$)\+
\\[0ex]\& $y$ = hd($L$) $\in$ $T$
\\[0ex]\& $x$ = last($L$) $\in$ $T$
\\[0ex]\& ($\forall$$i$:\{0..($\parallel$$L$$\parallel$ {-} 1)$^{-}$\}. $L$[$i$] = $f$($L$[($i$+1)]) $\in$ $T$ \& ($\neg$($L$[$i$] = $L$[($i$+1)] $\in$ $T$)))
\-
\end{tabbing}